\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it In}$:AbsInterface(${\it Cmd}$), ${\it Sys}$:AbsInterface(Top).
\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$).\+
\\[0ex]($\forall$$u$:E(${\it Sys}$). ($f$($u$) = $u$ $\in$ E) $\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E(${\it Sys}$).\+
\\[0ex]cr{-}explanation\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Sys}$; $f$; $e$)
\-\\[0ex]=
\\[0ex]cr{-}explanation\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Sys}$; $f$; ($f$($e$)))
\-\\[0ex]$\in$ (E(${\it In}$) List)))
\-\-
\end{tabbing}